dy>
Theory Term_Context
section â¹Preliminariesâº
theory Term_Context
imports First_Order_Terms.Term
Knuth_Bendix_Order.Subterm_and_Context
Polynomial_Factorization.Missing_List
begin
subsection â¹Additional functionality on @{type term} and @{type ctxt}âº
subsubsection â¹Positionsâº
type_synonym pos = "nat list"
context
notes conj_cong [fundef_cong]
begin
fun poss :: "('f, 'v) term â pos set" where
"poss (Var x) = {[]}"
| "poss (Fun f ss) = {[]} ⪠{i # p | i p. i < length ss â§ p â poss (ss ! i)}"
end
fun hole_pos where
"hole_pos â¡ = []"
| "hole_pos (More f ss D ts) = length ss # hole_pos D"
definition position_less_eq (infixl "â¤â©p" 67) where
"p â¤â©p q â· (â r. p @ r = q)"
abbreviation position_less (infixl "<â©p" 67) where
"p <â©p q â¡ p â q â§ p â¤â©p q"
definition position_par (infixl "â¥" 67) where
"p ⥠q ⷠ¬ (p â¤â©p q) ⧠¬ (q â¤â©p p)"
fun remove_prefix where
"remove_prefix (x # xs) (y # ys) = (if x = y then remove_prefix xs ys else None)"
| "remove_prefix [] ys = Some ys"
| "remove_prefix xs [] = None"
definition pos_diff (infixl "-â©p" 67) where
"p -â©p q = the (remove_prefix q p)"
fun subt_at :: "('f, 'v) term â pos â ('f, 'v) term" (infixl "|'_" 67) where
"s |_ [] = s"
| "Fun f ss |_ (i # p) = (ss ! i) |_ p"
| "Var x |_ _ = undefined"
fun ctxt_at_pos where
"ctxt_at_pos s [] = â¡"
| "ctxt_at_pos (Fun f ss) (i # p) = More f (take i ss) (ctxt_at_pos (ss ! i) p) (drop (Suc i) ss)"
| "ctxt_at_pos (Var x) _ = undefined"
fun replace_term_at ("_[_ â _]" [1000, 0, 0] 1000) where
"replace_term_at s [] t = t"
| "replace_term_at (Var x) ps t = (Var x)"
| "replace_term_at (Fun f ts) (i # ps) t =
(if i < length ts then Fun f (ts[i:=(replace_term_at (ts ! i) ps t)]) else Fun f ts)"
fun fun_at :: "('f, 'v) term â pos â ('f + 'v) option" where
"fun_at (Var x) [] = Some (Inr x)"
| "fun_at (Fun f ts) [] = Some (Inl f)"
| "fun_at (Fun f ts) (i # p) = (if i < length ts then fun_at (ts ! i) p else None)"
| "fun_at _ _ = None"
subsubsection â¹Computing the signatureâº
fun funas_term where
"funas_term (Var x) = {}"
| "funas_term (Fun f ts) = insert (f, length ts) (â (set (map funas_term ts)))"
fun funas_ctxt where
"funas_ctxt â¡ = {}"
| "funas_ctxt (More f ss C ts) = (â (set (map funas_term ss))) âª
insert (f, Suc (length ss + length ts)) (funas_ctxt C) ⪠(â (set (map funas_term ts)))"
subsubsection â¹Groundnessâº
fun ground where
"ground (Var x) = False"
| "ground (Fun f ts) = (â t â set ts. ground t)"
fun ground_ctxt where
"ground_ctxt â¡ â· True"
| "ground_ctxt (More f ss C ts) â· (â t â set ss. ground t) â§ ground_ctxt C â§ (â t â set ts. ground t)"
subsubsection â¹Depthâº
fun depth where
"depth (Var x) = 0"
| "depth (Fun f []) = 0"
| "depth (Fun f ts) = Suc (Max (depth ` set ts))"
subsubsection â¹Type conversionâº
text â¹We require a function which adapts the type of variables of a term,
so that states of the automaton and variables in the term language can be
chosen independently.âº
abbreviation "map_vars_term f ⡠map_term (λ x. x) f"
abbreviation "map_funs_term f ⡠map_term f (λ x. x)"
abbreviation "map_both f â¡ map_prod f f"
definition adapt_vars :: "('f, 'q) term â ('f,'v)term" where
[code del]: "adapt_vars ⡠map_vars_term (λ_. undefined)"
abbreviation "map_vars_ctxt f ⡠map_ctxt (λx. x) f"
definition adapt_vars_ctxt :: "('f,'q)ctxt â ('f,'v)ctxt" where
[code del]: "adapt_vars_ctxt = map_vars_ctxt (λ_. undefined)"
subsection â¹Properties of @{type pos}âº
lemma position_less_eq_induct [consumes 1]:
assumes "p â¤â©p q" and "â p. P p p"
and "â p q r. p â¤â©p q â¹ P p q â¹ P p (q @ r)"
shows "P p q" using assms
proof (induct p arbitrary: q)
case Nil then show ?case
by (metis append_Nil position_less_eq_def)
next
case (Cons a p)
then show ?case
by (metis append_Nil2 position_less_eq_def)
qed
text â¹We show the correspondence between the function @{const remove_prefix} and
the order on positions @{const position_less_eq}. Moreover how it can be used to
compute the difference of positions.âº
lemma remove_prefix_Nil [simp]:
"remove_prefix xs xs = Some []"
by (induct xs) auto
lemma remove_prefix_Some:
assumes "remove_prefix xs ys = Some zs"
shows "ys = xs @ zs" using assms
proof (induct xs arbitrary: ys)
case (Cons x xs)
show ?case using Cons(1)[of "tl ys"] Cons(2)
by (cases ys) (auto split: if_splits)
qed auto
lemma remove_prefix_append:
"remove_prefix xs (xs @ ys) = Some ys"
by (induct xs) auto
lemma remove_prefix_iff:
"remove_prefix xs ys = Some zs â· ys = xs @ zs"
using remove_prefix_Some remove_prefix_append
by blast
lemma position_less_eq_remove_prefix:
"p â¤â©p q â¹ remove_prefix p q â None"
by (induct rule: position_less_eq_induct) (auto simp: remove_prefix_iff)
text â¹Simplification rules on @{const position_less_eq}, @{const pos_diff},
and @{const position_par}.âº
lemma position_less_refl [simp]: "p â¤â©p p"
by (auto simp: position_less_eq_def)
lemma position_less_eq_Cons [simp]:
"(i # ps) â¤â©p (j # qs) â· i = j â§ ps â¤â©p qs"
by (auto simp: position_less_eq_def)
lemma position_less_Nil_is_bot [simp]: "[] â¤â©p p"
by (auto simp: position_less_eq_def)
lemma position_less_Nil_is_bot2 [simp]: "p â¤â©p [] â· p = []"
by (auto simp: position_less_eq_def)
lemma position_diff_Nil [simp]: "q -â©p [] = q"
by (auto simp: pos_diff_def)
lemma position_diff_Cons [simp]:
"(i # ps) -â©p (i # qs) = ps -â©p qs"
by (auto simp: pos_diff_def)
lemma Nil_not_par [simp]:
"[] ⥠p ⷠFalse"
"p ⥠[] ⷠFalse"
by (auto simp: position_par_def)
lemma par_not_refl [simp]: "p ⥠p ⷠFalse"
by (auto simp: position_par_def)
lemma par_Cons_iff:
"(i # ps) ⥠(j # qs) â· (i â j ⨠ps ⥠qs)"
by (auto simp: position_par_def)
text â¹Simplification rules on @{const poss}.âº
lemma Nil_in_poss [simp]: "[] â poss t"
by (cases t) auto
lemma poss_Cons [simp]:
"i # p â poss t â¹ [i] â poss t"
by (cases t) auto
lemma poss_Cons_poss:
"i # q â poss t â· i < length (args t) â§ q â poss (args t ! i)"
by (cases t) auto
lemma poss_append_poss:
"p @ q â poss t â· p â poss t â§ q â poss (t |_ p)"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons[of "args t ! i"] show ?case
by (cases t) auto
qed auto
text â¹Simplification rules on @{const hole_pos}âº
lemma hole_pos_map_vars [simp]:
"hole_pos (map_vars_ctxt f C) = hole_pos C"
by (induct C) auto
lemma hole_pos_in_ctxt_apply [simp]: "hole_pos C â poss Câ¨uâ©"
by (induct C) auto
subsection â¹Properties of @{const ground} and @{const ground_ctxt}âº
lemma ground_vars_term_empty [simp]:
"ground t â¹ vars_term t = {}"
by (induct t) auto
lemma ground_map_term [simp]:
"ground (map_term f h t) = ground t"
by (induct t) auto
lemma ground_ctxt_apply [simp]:
"ground Câ¨tâ© â· ground_ctxt C â§ ground t"
by (induct C) auto
lemma ground_ctxt_comp [intro]:
"ground_ctxt C â¹ ground_ctxt D â¹ ground_ctxt (C ââ©c D)"
by (induct C) auto
lemma ctxt_comp_n_pres_ground [intro]:
"ground_ctxt C â¹ ground_ctxt (C^n)"
by (induct n arbitrary: C) auto
lemma subterm_eq_pres_ground:
assumes "ground s" and "s âµ t"
shows "ground t" using assms(2,1)
by (induct) auto
lemma ground_substD:
"ground (l â
Ï) â¹ x â vars_term l â¹ ground (Ï x)"
by (induct l) auto
lemma ground_substI:
"(â x. x â vars_term s â¹ ground (Ï x)) â¹ ground (s â
Ï)"
by (induct s) auto
subsection â¹Properties on signature induced by a term @{type term}/context @{type ctxt}âº
lemma funas_ctxt_apply [simp]:
"funas_term Câ¨tâ© = funas_ctxt C ⪠funas_term t"
by (induct C) auto
lemma funas_term_map [simp]:
"funas_term (map_term f h t) = (λ (g, n). (f g, n)) ` funas_term t"
by (induct t) auto
lemma funas_term_subst:
"funas_term (l â
Ï) = funas_term l ⪠(â (funas_term ` Ï ` vars_term l))"
by (induct l) auto
lemma funas_ctxt_comp [simp]:
"funas_ctxt (C ââ©c D) = funas_ctxt C ⪠funas_ctxt D"
by (induct C) auto
lemma ctxt_comp_n_funas [simp]:
"(f, v) â funas_ctxt (C^n) â¹ (f, v) â funas_ctxt C"
by (induct n arbitrary: C) auto
lemma ctxt_comp_n_pres_funas [intro]:
"funas_ctxt C â â± â¹ funas_ctxt (C^n) â â±"
by (induct n arbitrary: C) auto
subsection â¹Properties on subterm at given position @{const subt_at}âº
lemma subt_at_Cons_comp:
"i # p â poss s â¹ (s |_ [i]) |_ p = s |_ (i # p)"
by (cases s) auto
lemma ctxt_at_pos_subt_at_pos:
"p â poss t â¹ (ctxt_at_pos t p)â¨uâ© |_ p = u"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) (auto simp: nth_append)
qed auto
lemma ctxt_at_pos_subt_at_id:
"p â poss t â¹ (ctxt_at_pos t p)â¨t |_ pâ© = t"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) force+
qed auto
lemma subst_at_ctxt_at_eq_termD:
assumes "s = t" "p â poss t"
shows "s |_ p = t |_ p â§ ctxt_at_pos s p = ctxt_at_pos t p" using assms
by auto
lemma subst_at_ctxt_at_eq_termI:
assumes "p â poss s" "p â poss t"
and "s |_p = t |_ p"
and "ctxt_at_pos s p = ctxt_at_pos t p"
shows "s = t" using assms
by (metis ctxt_at_pos_subt_at_id)
lemma subt_at_subterm_eq [intro!]:
"p â poss t â¹ t âµ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto
lemma subt_at_subterm [intro!]:
"p â poss t â¹ p â [] â¹ t â³ t |_ p"
proof (induct p arbitrary: t)
case (Cons i p)
from Cons(1)[of "args t ! i"] Cons(2) show ?case
by (cases t) force+
qed auto
lemma ctxt_at_pos_hole_pos [simp]: "ctxt_at_pos Câ¨sâ© (hole_pos C) = C"
by (induct C) auto
subsection â¹Properties on replace terms at a given position
@{const replace_term_at}âº
lemma replace_term_at_not_poss [simp]:
"p â poss s â¹ s[p â t] = s"
proof (induct s arbitrary: p)
case (Var x) then show ?case by (cases p) auto
next
case (Fun f ts) show ?case using Fun(1)[OF nth_mem] Fun(2)
by (cases p) (auto simp: min_def intro!: nth_equalityI)
qed
lemma replace_term_at_replace_at_conv:
"p â poss s â¹ (ctxt_at_pos s p)â¨tâ© = s[p â t]"
by (induct s arbitrary: p) (auto simp: upd_conv_take_nth_drop)
lemma parallel_replace_term_commute [ac_simps]:
"p ⥠q â¹ s[p â t][q â u] = s[q â u][p â t]"
proof (induct s arbitrary: p q)
case (Var x) then show ?case
by (cases p; cases q) auto
next
case (Fun f ts)
from Fun(2) have "p â []" "q â []" by auto
then obtain i j ps qs where [simp]: "p = i # ps" "q = j # qs"
by (cases p; cases q) auto
have "i â j â¹ (Fun f ts)[p â t][q â u] = (Fun f ts)[q â u][p â t]"
by (auto simp: list_update_swap)
then show ?case using Fun(1)[OF nth_mem, of j ps qs] Fun(2)
by (cases "i = j") (auto simp: par_Cons_iff)
qed
lemma replace_term_at_above [simp]:
"p â¤â©p q â¹ s[q â t][p â u] = s[p â u]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto
lemma replace_term_at_below [simp]:
"p <â©p q â¹ s[p â t][q â u] = s[p â t[q -â©p p â u]]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "tl q" "args s ! i"] Cons(2)
by (cases q; cases s) auto
qed auto
lemma replace_at_hole_pos [simp]: "Câ¨sâ©[hole_pos C â t] = Câ¨tâ©"
by (induct C) auto
subsection â¹Properties on @{const adapt_vars} and @{const adapt_vars_ctxt}âº
lemma adapt_vars2:
"adapt_vars (adapt_vars t) = adapt_vars t"
by (induct t) (auto simp add: adapt_vars_def)
lemma adapt_vars_simps[code, simp]: "adapt_vars (Fun f ts) = Fun f (map adapt_vars ts)"
by (induct ts, auto simp: adapt_vars_def)
lemma adapt_vars_reverse: "ground t â¹ adapt_vars t' = t â¹ adapt_vars t = t'"
unfolding adapt_vars_def
proof (induct t arbitrary: t')
case (Fun f ts)
then show ?case by (cases t') (auto simp add: map_idI)
qed auto
lemma ground_adapt_vars [simp]: "ground (adapt_vars t) = ground t"
by (simp add: adapt_vars_def)
lemma funas_term_adapt_vars[simp]: "funas_term (adapt_vars t) = funas_term t" by (simp add: adapt_vars_def)
lemma adapt_vars_adapt_vars[simp]: fixes t :: "('f,'v)term"
assumes g: "ground t"
shows "adapt_vars (adapt_vars t :: ('f,'w)term) = t"
proof -
let ?t' = "adapt_vars t :: ('f,'w)term"
have gt': "ground ?t'" using g by auto
from adapt_vars_reverse[OF gt', of t] show ?thesis by blast
qed
lemma adapt_vars_inj:
assumes "adapt_vars x = adapt_vars y" "ground x" "ground y"
shows "x = y"
using adapt_vars_adapt_vars assms by metis
lemma adapt_vars_ctxt_simps[simp, code]:
"adapt_vars_ctxt (More f bef C aft) = More f (map adapt_vars bef) (adapt_vars_ctxt C) (map adapt_vars aft)"
"adapt_vars_ctxt Hole = Hole" unfolding adapt_vars_ctxt_def adapt_vars_def by auto
lemma adapt_vars_ctxt[simp]: "adapt_vars (C ⨠t â© ) = (adapt_vars_ctxt C) ⨠adapt_vars t â©"
by (induct C, auto)
lemma adapt_vars_subst[simp]: "adapt_vars (l â
Ï) = l â
(λ x. adapt_vars (Ï x))"
unfolding adapt_vars_def
by (induct l) auto
lemma adapt_vars_gr_map_vars [simp]:
"ground t â¹ map_vars_term f t = adapt_vars t"
by (induct t) auto
lemma adapt_vars_gr_ctxt_of_map_vars [simp]:
"ground_ctxt C â¹ map_vars_ctxt f C = adapt_vars_ctxt C"
by (induct C) auto
subsubsection â¹Equality on ground terms/contexts by positions and symbolsâº
lemma fun_at_def':
"fun_at t p = (if p â poss t then
(case t |_ p of Var x â Some (Inr x) | Fun f ts â Some (Inl f)) else None)"
by (induct t p rule: fun_at.induct) auto
lemma fun_at_None_nposs_iff:
"fun_at t p = None â· p â poss t"
by (auto simp: fun_at_def') (meson term.case_eq_if)
lemma eq_term_by_poss_fun_at:
assumes "poss s = poss t" "âp. p â poss s â¹ fun_at s p = fun_at t p"
shows "s = t"
using assms
proof (induct s arbitrary: t)
case (Var x) then show ?case
by (cases t) simp_all
next
case (Fun f ss) note Fun' = this
show ?case
proof (cases t)
case (Var x) show ?thesis using Fun'(3)[of "[]"] by (simp add: Var)
next
case (Fun g ts)
have *: "length ss = length ts"
using Fun'(3) arg_cong[OF Fun'(2), of "λP. card {i |i p. i # p â P}"]
by (auto simp: Fun exI[of "λx. x â poss _", OF Nil_in_poss])
then have "i < length ss â¹ poss (ss ! i) = poss (ts ! i)" for i
using arg_cong[OF Fun'(2), of "λP. {p. i # p â P}"] by (auto simp: Fun)
then show ?thesis using * Fun'(2) Fun'(3)[of "[]"] Fun'(3)[of "_ # _ :: pos"]
by (auto simp: Fun intro!: nth_equalityI Fun'(1)[OF nth_mem, of n "ts ! n" for n])
qed
qed
lemma eq_ctxt_at_pos_by_poss:
assumes "p â poss s" "p â poss t"
and "â q. ¬ (p â¤â©p q) â¹ q â poss s â· q â poss t"
and "(â q. q â poss s ⹠¬ (p â¤â©p q) â¹ fun_at s q = fun_at t q)"
shows "ctxt_at_pos s p = ctxt_at_pos t p" using assms
proof (induct p arbitrary: s t)
case (Cons i p)
from Cons(2, 3) Cons(4, 5)[of "[]"] obtain f ss ts where [simp]: "s = Fun f ss" "t = Fun f ts"
by (cases s; cases t) auto
have flt: "j < i â¹ j # q â poss s â¹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have fgt: "i < j â¹ j # q â poss s â¹ fun_at s (j # q) = fun_at t (j # q)" for j q
by (intro Cons(5)) auto
have lt: "j < i â¹ j # q â poss s â· j # q â poss t" for j q by (intro Cons(4)) auto
have gt: "i < j â¹ j # q â poss s â· j # q â poss t" for j q by (intro Cons(4)) auto
from this[of _ "[]"] have "i < j â¹ j < length ss â· j < length ts" for j by auto
from this Cons(2, 3) have l: "length ss = length ts" by auto (meson nat_neq_iff)
have "ctxt_at_pos (ss ! i) p = ctxt_at_pos (ts ! i) p" using Cons(2, 3) Cons(4-)[of "i # q" for q]
by (intro Cons(1)[of "ss ! i" "ts ! i"]) auto
moreover have "take i ss = take i ts" using l lt Cons(2, 3) flt
by (intro nth_equalityI) (auto intro!: eq_term_by_poss_fun_at)
moreover have "drop (Suc i) ss = drop (Suc i) ts" using l Cons(2, 3) fgt gt[of "Suc i + j" for j]
by (intro nth_equalityI) (auto simp: nth_map intro!: eq_term_by_poss_fun_at, fastforce+)
ultimately show ?case by auto
qed auto
subsection â¹Miscâº
lemma fun_at_hole_pos_ctxt_apply [simp]:
"fun_at Câ¨tâ© (hole_pos C) = fun_at t []"
by (induct C) auto
lemma vars_term_ctxt_apply [simp]:
"vars_term Câ¨tâ© = vars_ctxt C ⪠vars_term t"
by (induct C arbitrary: t) auto
lemma map_vars_term_ctxt_apply:
"map_vars_term f Câ¨tâ© = (map_vars_ctxt f C)â¨map_vars_term f tâ©"
by (induct C) auto
lemma map_term_replace_at_dist:
"p â poss s â¹ (map_term f g s)[p â (map_term f g t)] = map_term f g (s[p â t])"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) (auto simp: nth_list_update intro!: nth_equalityI)
qed auto
endy>
Theory Basic_Utils
theory Basic_Utils
imports Term_Context
begin
primrec is_Inl where
"is_Inl (Inl q) â· True"
| "is_Inl (Inr q) â· False"
primrec is_Inr where
"is_Inr (Inr q) â· True"
| "is_Inr (Inl q) â· False"
fun remove_sum where
"remove_sum (Inl q) = q"
| "remove_sum (Inr q) = q"
text â¹List operationsâº
definition filter_rev_nth where
"filter_rev_nth P xs i = length (filter P (take (Suc i) xs)) - 1"
lemma filter_rev_nth_butlast:
"¬ P (last xs) ⹠filter_rev_nth P xs i = filter_rev_nth P (butlast xs) i"
unfolding filter_rev_nth_def
by (induct xs arbitrary: i rule: rev_induct) (auto simp add: take_Cons')
lemma filter_rev_nth_idx:
assumes "i < length xs" "P (xs ! i)" "ys = filter P xs"
shows "xs ! i = ys ! (filter_rev_nth P xs i) â§ filter_rev_nth P xs i < length ys"
using assms unfolding filter_rev_nth_def
proof (induct xs arbitrary: ys i)
case (Cons x xs) show ?case
proof (cases "P x")
case True
then obtain ys' where *:"ys = x # ys'" using Cons(4) by auto
show ?thesis using True Cons(1)[of "i - 1" ys'] Cons(2-)
unfolding *
by (cases i) (auto simp: nth_Cons' take_Suc_conv_app_nth)
next
case False
then show ?thesis using Cons(1)[of "i - 1" ys] Cons(2-)
by (auto simp: nth_Cons')
qed
qed auto
primrec add_elem_list_lists :: "'a â 'a list â 'a list list" where
"add_elem_list_lists x [] = [[x]]"
| "add_elem_list_lists x (y # ys) = (x # y # ys) # (map ((#) y) (add_elem_list_lists x ys))"
lemma length_add_elem_list_lists:
"ys â set (add_elem_list_lists x xs) â¹ length ys = Suc (length xs)"
by (induct xs arbitrary: ys) auto
lemma add_elem_list_listsE:
assumes "ys â set (add_elem_list_lists x xs)"
shows "â n ⤠length xs. ys = take n xs @ x # drop n xs" using assms
proof(induct xs arbitrary: ys)
case (Cons a xs)
then show ?case
by auto fastforce
qed auto
lemma add_elem_list_listsI:
assumes "n ⤠length xs" "ys = take n xs @ x # drop n xs"
shows "ys â set (add_elem_list_lists x xs)" using assms
proof (induct xs arbitrary: ys n)
case (Cons a xs)
then show ?case
by (cases n) (auto simp: image_iff)
qed auto
lemma add_elem_list_lists_def':
"set (add_elem_list_lists x xs) = {ys | ys n. n ⤠length xs ⧠ys = take n xs @ x # drop n xs}"
using add_elem_list_listsI add_elem_list_listsE
by fastforce
fun list_of_permutation_element_n :: "'a â nat â 'a list â 'a list list" where
"list_of_permutation_element_n x 0 L = [[]]"
| "list_of_permutation_element_n x (Suc n) L = concat (map (add_elem_list_lists x) (List.n_lists n L))"
lemma list_of_permutation_element_n_conv:
assumes "n â 0"
shows "set (list_of_permutation_element_n x n L) =
{xs | xs i. i < length xs â§ (â j < length xs. j â i â¶ xs ! j â set L) â§ length xs = n â§ xs ! i = x}" (is "?Ls = ?Rs")
proof (intro equalityI)
from assms obtain j where [simp]: "n = Suc j" using assms by (cases n) auto
{fix ys assume "ys â ?Ls"
then obtain xs i where wit: "xs â set (List.n_lists j L)" "i ⤠length xs"
"ys = take i xs @ x # drop i xs"
by (auto dest: add_elem_list_listsE)
then have "i < length ys" "length ys = Suc (length xs)" "ys ! i = x"
by (auto simp: nth_append)
moreover have "â j < length ys. j â i â¶ ys ! j â set L" using wit(1, 2)
by (auto simp: wit(3) min_def nth_append set_n_lists)
ultimately have "ys â ?Rs" using wit(1) unfolding set_n_lists
by auto}
then show "?Ls â ?Rs" by blast
next
{fix xs assume "xs â ?Rs"
then obtain i where wit: "i < length xs" "â j < length xs. j â i â¶ xs ! j â set L"
"length xs = n" "xs ! i = x"
by blast
then have *: "xs â set (add_elem_list_lists (xs ! i) (take i xs @ drop (Suc i) xs))"
unfolding add_elem_list_lists_def'
by (auto simp: min_def intro!: nth_equalityI)
(metis Cons_nth_drop_Suc Suc_pred append_Nil append_take_drop_id assms diff_le_self diff_self_eq_0 drop_take less_Suc_eq_le nat_less_le take0)
have [simp]: "x â set (take i xs) â¹ x â set L"
"x â set (drop (Suc i) xs) â¹ x â set L" for x using wit(2)
by (auto simp: set_conv_nth)
have "xs â ?Ls" using wit
by (cases "length xs")
(auto simp: set_n_lists nth_append * min_def
intro!: exI[of _ "take i xs @ drop (Suc i) xs"])}
then show "?Rs â ?Ls" by blast
qed
lemma list_of_permutation_element_n_iff:
"set (list_of_permutation_element_n x n L) =
(if n = 0 then {[]} else {xs | xs i. i < length xs â§ (â j < length xs. j â i â¶ xs ! j â set L) â§ length xs = n â§ xs ! i = x})"
proof (cases n)
case (Suc nat)
then have [simp]: "Suc nat â 0" by auto
then show ?thesis
by (auto simp: list_of_permutation_element_n_conv)
qed auto
lemma list_of_permutation_element_n_conv':
assumes "x â set L" "0 < n"
shows "set (list_of_permutation_element_n x n L) =
{xs. set xs â insert x (set L) â§ length xs = n â§ x â set xs}"
proof -
from assms(2) have *: "n â 0" by simp
show ?thesis using assms
unfolding list_of_permutation_element_n_conv[OF *]
by (auto simp: in_set_conv_nth)
(metis in_set_conv_nth insert_absorb subsetD)+
qed
text â¹Miscâº
lemma in_set_idx:
"x â set xs â¹ â i < length xs. xs ! i = x"
by (induct xs) force+
lemma set_list_subset_eq_nth_conv:
"set xs â A â· (â i < length xs. xs ! i â A)"
by (metis in_set_conv_nth subset_code(1))
lemma map_eq_nth_conv:
"map f xs = map g ys â· length xs = length ys â§ (â i < length ys. f (xs ! i) = g (ys ! i))"
using map_eq_imp_length_eq[of f xs g ys]
by (auto intro: nth_equalityI) (metis nth_map)
lemma nth_append_Cons: "(xs @ y # zs) ! i =
(if i < length xs then xs ! i else if i = length xs then y else zs ! (i - Suc (length xs)))"
by (cases i "length xs" rule: linorder_cases, auto simp: nth_append)
lemma map_prod_times:
"f ` A Ã g ` B = map_prod f g ` (A Ã B)"
by auto
lemma trancl_full_on: "(X Ã X)â§+ = X Ã X"
using trancl_unfold_left[of "X Ã X"] trancl_unfold_right[of "X Ã X"] by auto
lemma trancl_map:
assumes simu: "âx y. (x, y) â r â¹ (f x, f y) â s"
and steps: "(x, y) â râ§+"
shows "(f x, f y) â sâ§+" using steps
proof (induct)
case (step y z) show ?case using step(3) simu[OF step(2)]
by auto
qed (auto simp: simu)
lemma trancl_map_prod_mono:
"map_both f ` Râ§+ â (map_both f ` R)â§+"
proof -
have "(f x, f y) â (map_both f ` R)â§+" if "(x, y) â Râ§+" for x y using that
by (induct) (auto intro: trancl_into_trancl)
then show ?thesis by auto
qed
lemma trancl_map_both_Restr:
assumes "inj_on f X"
shows "(map_both f ` Restr R X)â§+ = map_both f ` (Restr R X)â§+"
proof -
have [simp]:
"map_prod (inv_into X f â f) (inv_into X f â f) ` Restr R X = Restr R X"
using inv_into_f_f[OF assms]
by (intro equalityI subrelI)
(force simp: comp_def map_prod_def image_def split: prod.splits)+
have [simp]:
"map_prod (f â inv_into X f) (f â inv_into X f) ` (map_both f ` Restr R X)â§+ = (map_both f ` Restr R X)â§+"
using f_inv_into_f[of _ f X] subsetD[OF trancl_mono_set[OF image_mono[of "Restr R X" "X Ã X" "map_both f"]]]
by (intro equalityI subrelI) (auto simp: map_prod_surj_on trancl_full_on comp_def rev_image_eqI)
show ?thesis using assms trancl_map_prod_mono[of f "Restr R X"]
image_mono[OF trancl_map_prod_mono[of "inv_into X f" "map_both f ` Restr R X"], of "map_both f"]
by (intro equalityI) (simp_all add: image_comp map_prod.comp)
qed
lemma inj_on_trancl_map_both:
assumes "inj_on f (fst ` R ⪠snd ` R)"
shows "(map_both f ` R)â§+ = map_both f ` Râ§+"
proof -
have [simp]: "Restr R (fst ` R ⪠snd ` R) = R"
by (force simp: image_def)
then show ?thesis using assms
using trancl_map_both_Restr[of f "fst ` R ⪠snd ` R" R]
by simp
qed
lemma kleene_induct:
"A â X â¹ B O X â X â¹ X O C â X â¹ Bâ§* O A O Câ§* â X"
using relcomp_mono[OF compat_tr_compat[of B X] subset_refl, of "Câ§*"] compat_tr_compat[of "C¯" "X¯"]
relcomp_mono[OF relcomp_mono, OF subset_refl _ subset_refl, of A X "Bâ§*" "Câ§*"]
unfolding rtrancl_converse converse_relcomp[symmetric] converse_mono by blast
lemma kleene_trancl_induct:
"A â X â¹ B O X â X â¹ X O C â X â¹ Bâ§+ O A O Câ§+ â X"
using kleene_induct[of A X B C]
by (auto simp: rtrancl_eq_or_trancl)
(meson relcomp.relcompI subsetD trancl_into_rtrancl)
lemma rtrancl_Un2_separatorE:
"B O A = {} â¹ (A ⪠B)â§* = Aâ§* ⪠Aâ§* O Bâ§*"
by (metis R_O_Id empty_subsetI relcomp_distrib rtrancl_U_push rtrancl_reflcl_absorb sup_commute)
lemma trancl_Un2_separatorE:
assumes "B O A = {}"
shows "(A ⪠B)â§+ = Aâ§+ ⪠Aâ§+ O Bâ§+ ⪠Bâ§+" (is "?Ls = ?Rs")
proof -
{fix x y assume "(x, y) â ?Ls"
then have "(x, y) â ?Rs" using assms
proof (induct)
case (step y z)
then show ?case
by (auto simp add: trancl_into_trancl relcomp_unfold dest: tranclD2)
qed auto}
then show ?thesis
by (auto simp add: trancl_mono)
(meson sup_ge1 sup_ge2 trancl_mono trancl_trans)
qed
text â¹Sum types where both components have the same type (to create copies)âº
lemma is_InrE:
assumes "is_Inr q"
obtains p where "q = Inr p"
using assms by (cases q) auto
lemma is_InlE:
assumes "is_Inl q"
obtains p where "q = Inl p"
using assms by (cases q) auto
lemma not_is_Inr_is_Inl [simp]:
"¬ is_Inl t ⷠis_Inr t"
"¬ is_Inr t ⷠis_Inl t"
by (cases t, auto)+
lemma [simp]: "remove_sum â Inl = id" by auto
abbreviation CInl :: "'q â 'q + 'q" where "CInl â¡ Inl"
abbreviation CInr :: "'q â 'q + 'q" where "CInr â¡ Inr"
lemma inj_CInl: "inj CInl" "inj CInr" using inj_Inl inj_Inr by blast+
lemma map_prod_simp': "map_prod f g G = (f (fst G), g (snd G))"
by (auto simp add: map_prod_def split!: prod.splits)
enddy>
Theory Ground_Terms
subsection â¹Ground constructionsâº
theory Ground_Terms
imports Basic_Utils
begin
subsubsection â¹Ground termsâº
text â¹This type serves two purposes. First of all, the encoding definitions and proofs are not
littered by cases for variables. Secondly, we can consider tree domains (usually sets of positions),
which become a special case of ground terms. This enables the construction of a term from a
tree domain and a function from positions to symbols.âº